#include "VariableChooser.cuh"
#include <math.h>

VariableChooser::VariableChooser(vector <Clause> * formula, int number_of_variables)
{
	this->formula = formula;
	this->evaluations = (Evaluation *) malloc(sizeof(Evaluation)*number_of_variables);
	this->number_of_variables = number_of_variables;
	this->evaluated = false;
	this->next_variable_index = number_of_variables - 1;

	for(int i = 0; i < number_of_variables; i++)
	{
		Var v = i;
		evaluations[i].variable = v;
		evaluations[i].evaluation = 0;
	}
}

VariableChooser::~VariableChooser()
{
	free(evaluations);
}

void VariableChooser::evaluate()
{
	for(int i = 0; i < formula->size(); i++)
	{
		Clause c = (*formula)[i];
		for(int j = 0; j < c.number_of_lits; j++)
		{
			Lit lit = c.literals[j];
			Var v = var(lit);

			int index = (int) v;

			evaluations[index].evaluation += v;

		}
	}

	quickSort(evaluations, 0, number_of_variables-1);

	evaluated = true;

}

Var VariableChooser::next_variable()
{
#ifdef USE_ASSERTIONS
	assert(evaluated && next_variable_index >= 0);
#endif

	Var v = evaluations[next_variable_index].variable;

	next_variable_index--;

	return v;

}

bool VariableChooser::has_next_variable()
{
#ifdef USE_ASSERTIONS
	assert(evaluated);
#endif

	return next_variable_index >= 0;
}
